package flowlogic;

import java.util.ArrayList;
import java.util.HashSet;

import ast.AtomicLabel;
import ast.Label;
import ast.LabelConjunction;
import ast.LabelDisjunction;
import ast.Term;

public class LabelJudgement extends FLJudgement {

	private Label label;
	private PsiNode psi;
	
	public LabelJudgement(Label lb)
	{
		label = lb;
		psi = new PsiNode();
	}
		
	public PsiNode getPsi() {
		return psi;
	}
	
	public String toString()
	{
		String res = "rho |- " + label + " : " + psi;
		return res;
	}

	public ArrayList<DischargeResult> discharge()
	{
		ArrayList<DischargeResult> resList = new ArrayList<DischargeResult>();
		
		if (label instanceof LabelConjunction) {
		
			ArrayList<Label> ops = ((LabelConjunction) label).getOps();
			LabelJudgement lbjgt = null;
			for (Label curLb : ops) {
				lbjgt = new LabelJudgement(curLb);
				resList.add(lbjgt);
				resList.add(new Inclusion(lbjgt.getPsi(), psi, true));
			}
			
		} else if (label instanceof LabelDisjunction) {
			
			ArrayList<Label> ops = ((LabelDisjunction) label).getOps();
			LabelJudgement lbjgt = null;
			for (Label curLb : ops) {
				lbjgt = new LabelJudgement(curLb);
				resList.add(lbjgt);
				resList.add(new Inclusion(lbjgt.getPsi(), psi, true));
			}
			
		} else if (label instanceof AtomicLabel) {
			
			// dealing with the owner term
			TermJudgement ojgt = new TermJudgement(((AtomicLabel) label).getOwner(), getRho());
			HashSet<Node> prSet = new HashSet<Node>();
			prSet.add(PrincipalTp.getInstance());
			HashSet<Node> srtSet = new HashSet<Node>();
			srtSet.add(SrtSignal.getInstance());
			resList.add(new GuardedConstraint(
					new Negation(new Inclusion(
									new TpNode(ojgt.getRes()), 
									new ConcreteSetNode(prSet), false)),
					new Inclusion(new ConcreteSetNode(srtSet), psi, true)));
			resList.add(new Inclusion(ojgt.getPsi(), psi, true));
			
			TermJudgement pjgt = null;
			for (Term ptrm : ((AtomicLabel) label).getInfluencers()) {
				pjgt = new TermJudgement(ptrm, getRho());
				resList.add(new GuardedConstraint(
					new Negation(new Inclusion(
									new TpNode(pjgt.getRes()),
									new ConcreteSetNode(prSet), false)),
					new Inclusion(new ConcreteSetNode(srtSet), psi, true)));
				resList.add(new Inclusion(pjgt.getPsi(), psi, true));
			}
			
		}
		
		return resList;
	}
	
}
